<html><body>
When sorting a set of text strings (for example, a file listing) jEdit
treats numbers specially, so for example "My file 10" will be placed after
"My file 2".
</body></html>
